\begin{tabbing}
$\forall$${\it es}$:ES, $x$, ${\it free}$:Id, $n$:$\mathbb{N}$, $e$:E.
\\[0ex]@loc($e$)($x$:Id)
\\[0ex]$\Rightarrow$ ($\neg$(($x$ after $e$) = ($x$ when $e$) $\in$ Id))
\\[0ex]$\Rightarrow$ $<$$n$, 0$>$ $<$ rank($e$)
\\[0ex]$\Rightarrow$ ($\exists$\=${\it e'}$:E\+
\\[0ex](${\it e'}$ $\leq$loc $e$ 
\\[0ex]\& rank(${\it e'}$) = $<$$n$, 1$>$ $\in$ (:$\mathbb{N}$ $\times$ $\mathbb{N}$)
\\[0ex]\& ($\neg$(($x$ after ${\it e'}$) = ($x$ when ${\it e'}$) $\in$ Id))
\\[0ex]\& (($\uparrow$$x$ changed before ${\it e'}$) $\Rightarrow$ (($x$ when ${\it e'}$) = ${\it free}$))))
\-
\end{tabbing}